n:, f:(n), m:n. sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n) 

latex

Definitions	AB, A, False, {i..j}, ij, P  Q, x:A. B(x), t  T, , i  j < k, P & Q, x(s), sum(f(x) | x < k), x. t(x), if b t else f fi, i=j, S  T, S  T, Dec(P), P  Q, Prop, SQType(T), {T}, Unit, P  Q, , b, b
Lemmas	sum functionality, assert wf, not wf, bnot wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, bool wf, decidable int equal, int seg wf, eq int wf, ifthenelse wf, sum wf, le wf, nat wf, nat properties, ge wf